Correttezza (logica matematica)

In logica matematica, la correttezza o validità (in inglese soundness) è una proprietà fondamentale delle regole logiche e dei calcoli logici.

Una regola logica (o regola di inferenza o regola di derivazione) è corretta se la conclusione è conseguenza logica delle (ossia, segue necessariamente dalle) premesse: se sono vere tutte le premesse allora è necessariamente vera la conclusione (o equivalentemente, non è possibile che le premesse siano tutte vere e la conclusione falsa). Ciò significa che, lette dall'alto verso il basso (dalle premesse alla conclusione), le regole logiche corrette preservano la verità, o equivalentemente, lette dal basso verso l'alto (dalla conclusione alle premesse) le regole logiche corrette preservano la falsità (se la conclusione è falsa, allora è necessariamente falsa almeno una delle premesse).

Un calcolo logico (ad esempio il calcolo dei sequenti o la deduzione naturale) è corretto in senso debole se ogni formula A derivabile in esso è valida, ossia se ogni formula A dimostrabile applicando un numero finito di volte le regole di derivazione del calcolo logico è vera per ogni modello. Un calcolo logico è corretto in senso forte se ogni formula A derivabile in esso a partire da un insieme di formule chiuse X (che fungono da assiomi di una teoria) è conseguenza logica di X. È evidente che la correttezza forte implica la correttezza debole: basta prendere per X un insieme vuoto di formule.

La correttezza è (assieme alla completezza semantica) un requisito essenziale di ogni calcolo logico, pertanto ciascuno di questi presenta un teorema di correttezza (debole o forte) che esprime appunto il fatto che tale calcolo logico è corretto (in senso debole o forte). Il teorema di correttezza debole (risp. forte) è il viceversa del teorema di completezza semantica debole (risp. forte).

Detto in modo intuitivo, un calcolo logico in quanto corretto è in grado di dimostrare solo le verità di una teoria, mentre in quanto completo (semanticamente) è in grado di dimostrare tutte le verità di una teoria.

Teorema di correttezza

Il teorema di correttezza (o soundness theorem) afferma che, per ogni insieme $\Gamma$ di formule ben formate (fbf), e per ogni fbf $\alpha$ , se esiste una dimostrazione di $\alpha$ il cui insieme di assunzioni "non scaricabili" è contenuto in $\Gamma$ , allora $\alpha$ è una conseguenza logica di $\Gamma$ , in simboli $\Gamma \vdash \alpha \implies \Gamma \vDash \alpha$ .

Dimostrazione

Dalla definizione di $\Gamma \vdash \alpha$ , è sufficiente provare che, per ogni derivazione ${\mathcal {D}}$ , vale $\Gamma \vdash _{\mathcal {D}}\alpha \implies \Gamma \vDash \alpha$ , dove $\Gamma \vdash _{\mathcal {D}}\alpha$ significa che ${\mathcal {D}}$ è una dimostrazione di $\alpha$ da $\Gamma$ . Si procederà per induzione sulle derivazioni ${\mathcal {D}}$ di $\alpha$ da $\Gamma$ .

${\mathcal {D}}$ è una derivazione atomica, cioè $\alpha$ è una dimostrazione di $\alpha$ da $\Gamma$ . In altre parole, $\alpha \in \Gamma$ . A fortiori, $\Gamma \vDash \alpha$ .
${\mathcal {D}}$ è una derivazione della forma ${\frac {\Gamma '\vdash _{{\mathcal {D}}_{1}}\gamma \;\;\;\;\;\;\;\Gamma ''\vdash _{{\mathcal {D}}_{2}}\delta }{\gamma \land \delta }}$ , dove $\gamma \land \delta =:\alpha$ . Siano $\Gamma '$ e $\Gamma ''$ le assunzioni utilizzate in ${\mathcal {D}}_{1}$ e in ${\mathcal {D}}_{2}$ rispettivamente. Allora $\Gamma '\cup \Gamma '\subseteq \Gamma$ . Dal primo ramo della derivazione ${\mathcal {D}}$ , si ha $\Gamma '\vdash _{{\mathcal {D}}_{1}}\alpha$ , da cui, per ipotesi induttiva, segue $\Gamma '\vDash \gamma$ . Allo stesso modo $\Gamma '\vDash \delta$ . In conclusione, essendo $\Gamma '\cup \Gamma '\subseteq \Gamma$ , segue $\Gamma \vDash \gamma$ e $\Gamma \vDash \delta$ , da cui $\Gamma \vDash \gamma \land \delta =\alpha$ .
${\mathcal {D}}$ è una derivazione della forma ${\frac {\Gamma ,[\neg \alpha ]\vdash _{\mathcal {D_{1}}}\bot }{\alpha }}$ . Per ipotesi induttiva, segue $\Gamma ,\neg \alpha \vDash \bot$ . In altre parole, per ogni valutazione $\nu$ , si ha

\nu (\Gamma \cup \{\neg \alpha \})=1\implies \nu (\bot )=1.

Dal fatto che

\nu (\bot )=0

, segue che

\nu (\Gamma \cup \{\neg \alpha \})=0

, per ogni valutazione

\nu

. Questo significa che, ogni qual volta

\nu (\Gamma )=1

, si ha

\nu (\neg \alpha )=0

, cioè

\nu (\alpha )=1

. Quindi

\Gamma \vDash \alpha

.

${\mathcal {D}}$ è una derivazione della forma ${\frac {\Gamma \vdash _{{\mathcal {D}}_{2}}\gamma \lor \delta \;\;\;\;\;\;\;\Gamma ,[\gamma ]\vdash _{{\mathcal {D}}_{2}}\alpha \;\;\;\;\;\;\;\Gamma ,[\delta ]\vdash _{{\mathcal {D}}_{3}}\alpha }{\alpha }}$ . Per ipotesi induttiva, segue $\Gamma \vDash \gamma \lor \delta$ . Similmente, si ottiene $\Gamma ,\gamma \vDash \alpha$ e $\Gamma ,\delta \vDash \alpha$ . Sia $\nu$ una valutazione tale che $\nu (\Gamma )=1$ . Allora $\nu (\gamma \lor \delta )=1$ , ovvero $\nu (\gamma )=1$ o $\nu (\delta )=1$ . Se $\nu (\gamma )=1$ , e dal fatto che $\Gamma ,\gamma \vDash \alpha$ , segue $\nu (\alpha )=1$ . Analogamente, se $\nu (\delta )=1$ , e dal fatto che $\Gamma ,\delta \vDash \alpha$ , segue $\nu (\alpha )=1$ . In conclusione, $\Gamma \vDash \alpha$ .